| Definitions | Top, Type, t  T,  x:A. B(x), w.M, f(a), AtomFree(T;x), Id, x:A  B(x), IdLnk, w.TA, x:A B(x), P & Q, w.T, <a,b>, w-atom-constraint(w), Void,  x:A. B(x), Unit,  , FairFifo, P   Q, World, world-es-atom, E, s = t, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val),  ,  b,  A, {x:A| B(x) }, world-es-val,   x. t(x), 1of(t), 2of(t), a(i;t), kind(a), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), False, A B,  , act(e), time(e), kind(e), P  Q, P Q, {T}, SQType(T), V(i;k), val(e), Msg(M), S  T, type List, Knd, S  T, w-automaton(T;TA;M), w-machine(w;i), vartype(i;x), #$n, a<b, s(i;t).x, w-pred(w;e), left+right, kind(e), EOrderAxioms(E; pred?; info), pred!(e;e'), SWellFounded(R(x;y)), first(e), w-order-axioms, strong-subtype(A;B), isnull(a), Prop, EqDecider(T), NatDeq, IdDeq, product-deq(A;B;a;b), ES(the_w), ES, loc(e), w-info(w;e), x.A(x), loc(e), s ~ t |